package at.ptasat;

import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.OutputStream;
import java.io.PrintStream;
import java.util.ArrayList;
import java.util.List;

import at.ptasat.Configuration.ArgumentConfig;
import at.ptasat.Configuration.PipeMode;
import at.ptasat.solver.AsyncSolver;
import at.ptasat.solver.AsyncSolverListener;
import at.ptasat.util.BufferingOutputStream;
import at.ptasat.util.NullOutputStream;
import at.tasat.io.OutputFormatter;

public final class Main {

	public static void main(String[] args) {
		Configuration config = Configuration.get(args);
		int code = main(config);
		System.exit(code);
	}

	public static int main(final Configuration config) {
		final boolean verbose = config.isVerboseStatus();
		final PrintStream out = new PrintStream(config.getOut());
		final PrintStream err = new PrintStream(config.getErr());
		ArgumentConfig[] configs = config.getArgumentConfigs();
		final List<AsyncSolver> solvers = new ArrayList<AsyncSolver>(configs.length);
		try {
			if (config.isVerboseConfig()) {
				out.println(OutputFormatter.getCommentString(config.toString()));
			}
			log(verbose, out, "creating workers");
			File file = config.isInFile() ? config.getInFile() : writeToTempFile(config.getIn());
			Handler handler = new Handler(out, err, config.isVerboseWinner());
			loop: for (ArgumentConfig c : configs) {
				for (int i = 0; i < c.nInstances; i++) {
					final OutputStream solverOut = createSolverStream(config.getOut(), config.getOutPipeMode());
					final OutputStream solverErr = createSolverStream(config.getErr(), config.getErrPipeMode());
					solvers.add(config.getFactory().create(handler, solverOut, solverErr, c.argument));
					if (config.getMax() > 0 && solvers.size() >= config.getMax()) {
						break loop;
					}
				}
			}
			log(verbose, out, "starting workers");
			for (AsyncSolver solver : solvers) {
				StringBuilder additionalArgument = new StringBuilder();
				for (String globalArgument : config.getGlobalArguments()) {
					additionalArgument.append(globalArgument);
					additionalArgument.append(' ');
				}
				if (!solver.getArguments().contains("--seed") && !solver.getArguments().contains("-s")) {
					additionalArgument.append("--seed=" + config.getRandom().nextLong());
					additionalArgument.append(' ');
				}
				if (config.isVerboseWorker()) {
					out.println(OutputFormatter.getCommentString("worker " + solver.getId() + ": \"" + additionalArgument + " " + solver.getArguments() + "\""));
				}
				log(verbose, out, "starting worker %d: (\"%s\")", solver.getId(), solver.getArguments());
				solver.start(additionalArgument.toString().trim(), file);
				log(verbose, out, "started worker %d: (\"%s\")", solver.getId(), solver.getArguments());
			}
			log(verbose, out, "started %d workers", solvers.size());
			log(verbose, out, "waiting for workers");
			synchronized (handler) {
				while (!handler.isFinished()) {
					handler.wait();
				}
			}
			log(verbose, out, "finished");
			return 0;
		} catch (Throwable t) {
			log(verbose, err, "failed");
			err.println(OutputFormatter.getErrorString(t));
			return 1;
		} finally {
			log(verbose, out, "killing all workers");
			for (AsyncSolver solver : solvers) {
				log(verbose, out, "killing worker %d", solver.getId());
				solver.kill();
				log(verbose, out, "killed worker %d", solver.getId());
			}
			log(verbose, out, "killed all workers");
		}
	}

	private static File writeToTempFile(InputStream in) throws IOException, FileNotFoundException {
		File file = File.createTempFile("p-tasat_", "cnf");
		OutputStream tmp = new FileOutputStream(file);
		byte[] buffer = new byte[4096];
		for (int nBytes = in.read(buffer); nBytes > 0; nBytes = in.read(buffer)) {
			tmp.write(buffer, 0, nBytes);
		}
		tmp.close();
		return file;
	}

	private static void log(boolean verbose, PrintStream out, String msg, Object... args) {
		if (verbose) {
			out.println(OutputFormatter.getCommentString(String.format(msg.trim(), args)));
		}
	}

	private static OutputStream createSolverStream(OutputStream out, PipeMode mode) {
		switch (mode) {
		case IMMEDIATE:
			return out;
		case LATE_ON_SELF_TERMINATION:
			return new BufferingOutputStream(out);
		case SILENT:
			return new NullOutputStream();
		default:
			throw new IllegalArgumentException();
		}
	}

	private static final class Handler implements AsyncSolverListener {

		private final PrintStream out, err;
		private final boolean isVerboseWinner;
		private int nSolvers;
		private int nFinished;
		private boolean finished;

		public Handler(PrintStream out, PrintStream err, boolean isVerboseWinner) {
			this.out = out;
			this.err = err;
			this.nSolvers = 0;
			this.isVerboseWinner = isVerboseWinner;
			nFinished = 0;
			finished = false;
		}

		public boolean isFinished() {
			return finished;
		}

		@Override
		public synchronized void enroll(AsyncSolver sender) {
			nSolvers++;
		}

		@Override
		public synchronized void solved(AsyncSolver sender) {
			if (!finished) {
				nFinished++;
				finished = true;
				notifyAll();
				try {
					sender.getErr().flush();
					sender.getOut().flush();
				} catch (IOException e) {
					// nothing to do
				}
				if (isVerboseWinner) {
					out.println(OutputFormatter.getCommentString("winner: worker " + sender.getId() + " (\"" + sender.getArguments() + "\")"));
				}
			}
		}

		@Override
		public synchronized void failed(AsyncSolver sender) {
			if (!finished) {
				nFinished++;
				finished |= nFinished >= nSolvers;
				if (finished) {
					notifyAll();
				}
				try {
					sender.getOut().flush();
					sender.getErr().flush();
				} catch (IOException e) {
					// nothing to do
				}
				err.println(OutputFormatter.getErrorString("failed: worker " + sender.getId() + " (\"" + sender.getArguments() + "\")"));
			}
		}
	}

}
